/*
 * Formula.h
 *
 *  Created on: May 2, 2012
 *      Author: lorenzo
 */

#ifndef FORMULA_H_
#define FORMULA_H_

#include <vector>
#include "Clause.h"
#include "EvaluationReport.h"

struct literal{
	unsigned int index;
	bool negation;
};

typedef struct literal lit;

class Literal;
class Clause;
class EvaluationReport;

class Formula {
public:
	Formula();
	virtual ~Formula();

	void addClause(std::vector<Literal> & literals);
	bool evaluate();
	EvaluationReport getEvaluationReport();
	unsigned int countSatisfiedClauses();
	unsigned int countClauses();
	void setVar(unsigned int index, bool value);
	unsigned int varsCount();
	bool getVarValue(unsigned int index);
	std::vector<bool> getVarSetting();
	bool hasEmptyClause();

private:
	std::vector<Clause> clauses;
	std::vector<bool> vars;
};

#endif /* FORMULA_H_ */
